$\forall$$T$:Type, $L_{1}$, $L_{2}$, $L$:($T$ List), $x$:$T$.
\\[0ex]no\_repeats($T$;$L$) $\Rightarrow$ $L_{1}$ @ [$x$] $\subseteq$ $L$ $\Rightarrow$ [$x$ / $L_{2}$] $\subseteq$ $L$ $\Rightarrow$ $L_{1}$ @ [$x$ / $L_{2}$] $\subseteq$ $L$